Requirements-Based Programming (RBP) has been advocated as a viable means of developing complex, evolving systems. In RBP, requirements can be systematically transformed into executable computer instructions. An implementation of RBP provides a way to generate executable computer instructions from requirements with neither the time involved in manually writing the executable computer instructions, nor the mistakes regarded (generally speaking) as unavoidable in manually writing the executable computer instructions.
Complex systems in general cannot attain high dependability without addressing the crucial remaining open issues of software dependability. The need for ultrahigh dependability systems increases continually, along with a correspondingly increasing need to ensure correctness in system development. Correctness exists where the implemented system is equivalent to the requirements, and where this equivalence can be proved mathematically.
Development of a system that will have a high level of reliability requires the developer to represent the system as a formal model that can be proven to be correct.
Conventional system development tools and methods that are based on formal models provide neither automated generation of the models from requirements nor automated proof of correctness of the models. Conventional system development tools and methods provide no automated, generally applicable way to produce a system—or even a procedure—that is a provably correct implementation of the customer's requirements. Furthermore, requirements engineering as a discipline has yet to produce an automated, mathematics-based process for requirements validation. Automatic code generation from requirements has been the ultimate objective of software engineering almost since the advent of high-level programming languages, and calls for capability of “requirements-based programming” have become strong.
Several tools and products exist in the marketplace today for automatic code generation from a given model; however, these tools and products typically generate code, portions of which are never executed, or portions of which cannot be justified from either the requirements or the model. Moreover, existing tools do not and cannot overcome the fundamental inadequacy of all currently available automated development approaches, which is that they include no way to establish a provable equivalence between the requirements stated at the outset and either the model or the code they generate.
In particular, one tool for deriving executable code from informal notations requires translating the informal specifications into traces, and then using an automated theorem prover to infer an equivalent process-based description. Traces are sequences of events that have occurred in a particular ordering up to a particular point in time. Inferring an equivalent process based specification from the traces requires large computational facilities, sometimes even as large as a supercomputer.
Traditional approaches to automatic code generation, including those embodied in commercial products such as Matlab®, in system development toolsets such as the B-Toolkit® or the VDM++® toolkit, or in academic research projects, presuppose the existence of an explicit (formal) model of reality that can be used as the basis for subsequent code generation. However, these traditional approaches not only depend on other ways to provide the explicit formal model, but also include no facility to ascertain or establish that the model corresponds to the customer's requirements. While such an approach is reasonable, the advantages and disadvantages of the various modeling approaches used in computing are well known, and certain models can serve well to highlight certain issues while suppressing other, less-relevant details. The converse is also true. Certain models of reality, while successfully detailing many of the issues of interest to developers, can fail to capture some important issues, or perhaps even the most important issues. Existing reverse-engineering approaches suffer from a similar plight. In typical approaches, a model is extracted from an existing system and is then represented in various ways, for example as a digraph. The re-engineering process then involves using the resulting representation as the basis for code generation, as indicated above.
The model on which automatic code generation is based is referred to as a design, or more correctly, a design specification. There is typically a mismatch between this design specification and the implementation (sometimes termed the “specification-implementation gap”) in that the process of going from a suitable design to an implementation involves many practical decisions that must be made by the automated tool used for code generation without any clear-cut justifications other than the predetermined implementation decisions of the tool designers. Further, there is a more problematic “gap,” termed the “analysis-specification gap,” that emphasizes the problem of capturing requirements and adequately representing them in a specification that is clear, concise, and complete. This specification must be formal, or proof of correctness is impossible.
Unfortunately, many software system designers are reluctant to embrace formal specification techniques, believing the formal specification techniques to be difficult to use and apply, despite many industrial success stories. While software system designers are happy to write descriptions as natural language scenarios, or even using semi-formal notations such as unified modeling language (UML) use cases, the software system designers are reticent to undertake formal specification. However, absent a formal specification of the system under consideration, there is no possibility of determining any acceptable level of confidence in the correctness of an implementation. More importantly, formal specification must be ensured to have fully, completely, and consistently captured the prescribed requirements. System requirements cannot be expected to be perfect, complete, and consistent from the outset, which is why it is even more important to have a formal specification. Such a formal specification can highlight errors, omissions, and conflicts. The formal specification must also reflect changes and updates from system maintenance, as well as changes and compromises in requirements, so that it remains an accurate representation of the system throughout the life cycle of a system.
Requirements typically evolve during the life cycle of a system, Manual change to the system creates a risk of introducing new errors and necessitates retesting and revalidation, which can greatly increase the cost of the system. Often, needed changes are not made due to the cost of making consequential changes in the rest of the system. Sometimes changes are simply made in the code and not reflected in the specification or design due to the cost or due to the fact that those who generated the original specification or design are no longer available.
For the reasons stated above, and for other reasons stated below which will become apparent to those skilled in the art upon reading and understanding the present specification, there is a need in the art for an automated, generally applicable approach to produce a system that is a provably correct implementation of an informal design specification that does not require use of a theorem-prover. There is a further need for a convenient way of generating a new system when system requirements change. There is also a need for an automated, mathematics-based process for requirements validation that does not require large computational facilities.